<html>
<head><meta charset="utf-8"><title>Extracting borrow information from mir_borrowck · t-compiler · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/131828-t-compiler/index.html">t-compiler</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck.html">Extracting borrow information from mir_borrowck</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="228539937"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/131828-t-compiler/topic/Extracting%20borrow%20information%20from%20mir_borrowck/near/228539937" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck.html#228539937">(Mar 03 2021 at 05:37)</a>:</h4>
<p>I'm interested in building a <a href="https://en.wikipedia.org/wiki/Program_slicing">program slicer</a> for Rust. I originally <a href="#narrow/stream/185405-t-compiler.2Fwg-rls-2.2E0/topic/Program.20slicing.20in.20RA/near/228018712">proposed doing this</a> for rust-analyzer, but I need access to the computed borrow information about the MIR, so I decided to hook into the compiler directly. However, much to my chagrin, the compiler doesn't expose borrow information. As far as I can tell, <code>mir_borrowck</code> keeps all the borrow information internally. The returned <code>BorrowCheckResult</code> doesn't have much information.</p>
<p>Does anyone have a sense of roughly what would be involved in changing the <code>mir_borrowck</code> interface to return more information? Would it be just a matter of moving the internal data structures like <a href="https://github.com/rust-lang/rust/blob/35dbef235048f9a2939dc20effe083ca483c37ff/compiler/rustc_mir/src/borrow_check/mod.rs#L206"><code>RegionInferenceContext</code></a> into the return signature? I tried doing that with the <a href="https://github.com/rust-lang/rust/blob/35dbef235048f9a2939dc20effe083ca483c37ff/compiler/rustc_mir/src/borrow_check/mod.rs#L202"><code>BorrowSet</code></a>, but ran into several issues on making it hashable.</p>



<a name="228540157"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/131828-t-compiler/topic/Extracting%20borrow%20information%20from%20mir_borrowck/near/228540157" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Joshua Nelson <a href="https://rust-lang.github.io/zulip_archive/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck.html#228540157">(Mar 03 2021 at 05:40)</a>:</h4>
<p>prusti does this with <a href="#narrow/stream/185405-t-compiler.2Fwg-rls-2.2E0/topic/Program.20slicing.20in.20RA/near/228069017">really awful hacks</a></p>



<a name="228540184"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/131828-t-compiler/topic/Extracting%20borrow%20information%20from%20mir_borrowck/near/228540184" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Joshua Nelson <a href="https://rust-lang.github.io/zulip_archive/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck.html#228540184">(Mar 03 2021 at 05:40)</a>:</h4>
<p>I don't know if anyone's tried to make it usable from a library</p>



<a name="228593624"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/131828-t-compiler/topic/Extracting%20borrow%20information%20from%20mir_borrowck/near/228593624" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck.html#228593624">(Mar 03 2021 at 13:49)</a>:</h4>
<p>Yes, I talked with <span class="user-mention" data-user-id="116109">@Vytautas Astrauskas [he/him]</span> about this. The only issue is that Prusti can't scrape all the information that rustc infers, because it's limited to whatever is output in the logs. I'm interested in extracting all the computed information so my analysis pass has access to it.</p>



<a name="228601585"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/131828-t-compiler/topic/Extracting%20borrow%20information%20from%20mir_borrowck/near/228601585" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Joshua Nelson <a href="https://rust-lang.github.io/zulip_archive/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck.html#228601585">(Mar 03 2021 at 14:36)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> might be a good person to ask, but AFAIK turning borrowck into a library is still a long way off, no one is working on it</p>



<a name="228610231"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/131828-t-compiler/topic/Extracting%20borrow%20information%20from%20mir_borrowck/near/228610231" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck.html#228610231">(Mar 03 2021 at 15:24)</a>:</h4>
<p><span class="user-mention silent" data-user-id="232545">Joshua Nelson</span> <a href="#narrow/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck/near/228540157">said</a>:</p>
<blockquote>
<p>prusti does this with <a href="#narrow/stream/185405-t-compiler.2Fwg-rls-2.2E0/topic/Program.20slicing.20in.20RA/near/228069017">really awful hacks</a></p>
</blockquote>
<p>To my understanding, the minimal thing we need to be able to remove these hacks is the ability to get lifetime constraints for function calls at MIR optimized level. If someone would agree to mentor the creation of API that allows getting these lifetime constraints, I could try to find a summer intern to work on this.</p>



<a name="228695221"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/131828-t-compiler/topic/Extracting%20borrow%20information%20from%20mir_borrowck/near/228695221" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck.html#228695221">(Mar 04 2021 at 00:37)</a>:</h4>
<p>my plan was to do it through polonius</p>



<a name="228695231"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/131828-t-compiler/topic/Extracting%20borrow%20information%20from%20mir_borrowck/near/228695231" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck.html#228695231">(Mar 04 2021 at 00:37)</a>:</h4>
<p>but I suppose we could expose it from MIR borrowck in some other way</p>



<a name="228748563"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/131828-t-compiler/topic/Extracting%20borrow%20information%20from%20mir_borrowck/near/228748563" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck.html#228748563">(Mar 04 2021 at 10:30)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116009">nikomatsakis</span> <a href="#narrow/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck/near/228695221">said</a>:</p>
<blockquote>
<p>my plan was to do it through polonius</p>
</blockquote>
<p>Polonius would be an option if there was a way to access the version of MIR on which Polonius is running. (Together with all information necessary to map Polonius facts to MIR elements such as lifetime identifiers and MIR locations.)</p>



<a name="228748747"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/131828-t-compiler/topic/Extracting%20borrow%20information%20from%20mir_borrowck/near/228748747" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck.html#228748747">(Mar 04 2021 at 10:32)</a>:</h4>
<p>By the way, going via the file system can have a huge performance impact, so it would be good to avoid that, too.</p>



<a name="228754741"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/131828-t-compiler/topic/Extracting%20borrow%20information%20from%20mir_borrowck/near/228754741" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck.html#228754741">(Mar 04 2021 at 11:22)</a>:</h4>
<p>it's probably a good idea for me to be specific about what I mean by "do it through polonius"</p>



<a name="228754747"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/131828-t-compiler/topic/Extracting%20borrow%20information%20from%20mir_borrowck/near/228754747" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck.html#228754747">(Mar 04 2021 at 11:22)</a>:</h4>
<p>I'm not even 100% sure I know :)</p>



<a name="228754762"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/131828-t-compiler/topic/Extracting%20borrow%20information%20from%20mir_borrowck/near/228754762" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck.html#228754762">(Mar 04 2021 at 11:22)</a>:</h4>
<p>I think I meant: communicate via polonius facts?</p>



<a name="228754776"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/131828-t-compiler/topic/Extracting%20borrow%20information%20from%20mir_borrowck/near/228754776" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck.html#228754776">(Mar 04 2021 at 11:23)</a>:</h4>
<p>I have to think about this</p>



<a name="228929115"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/131828-t-compiler/topic/Extracting%20borrow%20information%20from%20mir_borrowck/near/228929115" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck.html#228929115">(Mar 05 2021 at 10:14)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116009">nikomatsakis</span> <a href="#narrow/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck/near/228754762">said</a>:</p>
<blockquote>
<p>I think I meant: communicate via polonius facts?</p>
</blockquote>
<p>Something like <code>tcx.get_polonius_facts(def_id)</code>?</p>
<p>Just a side comment: With Prusti we are currently trying to dive into the verification of unsafe code. Therefore, we need Polonius input facts, not its output facts.</p>



<a name="228929175"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/131828-t-compiler/topic/Extracting%20borrow%20information%20from%20mir_borrowck/near/228929175" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck.html#228929175">(Mar 05 2021 at 10:14)</a>:</h4>
<p>If you would like to have a call to discuss this, let me know.</p>



<a name="229093511"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/131828-t-compiler/topic/Extracting%20borrow%20information%20from%20mir_borrowck/near/229093511" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> oliver <a href="https://rust-lang.github.io/zulip_archive/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck.html#229093511">(Mar 06 2021 at 12:18)</a>:</h4>
<p>how will you be verifying the unsafe code?</p>



<a name="229192704"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/131828-t-compiler/topic/Extracting%20borrow%20information%20from%20mir_borrowck/near/229192704" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck.html#229192704">(Mar 07 2021 at 14:43)</a>:</h4>
<p><span class="user-mention silent" data-user-id="281739">oliver</span> <a href="#narrow/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck/near/229093511">said</a>:</p>
<blockquote>
<p>how will you be verifying the unsafe code?</p>
</blockquote>
<p>We still trying to figure this out.</p>



<a name="230277703"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/131828-t-compiler/topic/Extracting%20borrow%20information%20from%20mir_borrowck/near/230277703" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/131828-t-compiler/topic/Extracting.20borrow.20information.20from.20mir_borrowck.html#230277703">(Mar 14 2021 at 23:11)</a>:</h4>
<p>Not directly on topic for the thread, but just for fun -- I've been able to get pretty far with my program slicer without using any borrow information. For example, this program shows a slice on the variable "total" in the last line.</p>
<p><a href="/user_uploads/4715/VxTrZQOP9bVoOEFZXCq8zRSg/Screen-Shot-2021-03-14-at-7.08.28-PM.png">Screen-Shot-2021-03-14-at-7.08.28-PM.png</a> </p>
<div class="message_inline_image"><a href="/user_uploads/4715/VxTrZQOP9bVoOEFZXCq8zRSg/Screen-Shot-2021-03-14-at-7.08.28-PM.png" title="Screen-Shot-2021-03-14-at-7.08.28-PM.png"><img src="/user_uploads/4715/VxTrZQOP9bVoOEFZXCq8zRSg/Screen-Shot-2021-03-14-at-7.08.28-PM.png"></a></div><p>And this program shows a slice on "input" in the line <code>input == "exit"</code>.</p>
<p><a href="/user_uploads/4715/ZhEKX2MQnVy8UKViAOGc9v4B/Screen-Shot-2021-03-14-at-7.09.07-PM.png">Screen-Shot-2021-03-14-at-7.09.07-PM.png</a></p>
<div class="message_inline_image"><a href="/user_uploads/4715/ZhEKX2MQnVy8UKViAOGc9v4B/Screen-Shot-2021-03-14-at-7.09.07-PM.png" title="Screen-Shot-2021-03-14-at-7.09.07-PM.png"><img src="/user_uploads/4715/ZhEKX2MQnVy8UKViAOGc9v4B/Screen-Shot-2021-03-14-at-7.09.07-PM.png"></a></div>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>